// ***** This file is automatically generated from Range.java.jpp

package daikon.inv.unary.scalar;

import daikon.*;
import daikon.inv.*;
import daikon.inv.unary.sequence.*;
import daikon.inv.binary.sequenceScalar.*;
import daikon.derive.unary.*;
import daikon.Quantify.QuantFlags;

import java.util.*;
import java.util.logging.Logger;
import java.util.logging.Level;
import plume.*;

/**
 * Baseclass for unary range based invariants.  Each invariant is a
 * special stateless version of bound or oneof.  For example
 * EqualZero, BooleanVal, etc). These are never printed, but are used
 * internally as suppressors for ni-suppressions.
 *
 * Each specific invariant is implemented in a subclass (typically in
 * this file).
 */

public abstract class RangeFloat extends SingleFloat {

  // We are Serializable, so we specify a version to allow changes to
  // method signatures without breaking serialization.  If you add or
  // remove fields, you should change this number to the current date.
  static final long serialVersionUID = 20040311L;

  protected RangeFloat (PptSlice ppt) {
    super (ppt);
  }

  protected /*@Prototype*/ RangeFloat () {
    super ();
  }

  /**
   * Check that instantiation is ok.  The type must be integral
   * (not boolean or hash code)
   */
  public boolean instantiate_ok (VarInfo[] vis) {

    if (!valid_types (vis))
      return (false);

    if (!vis[0].file_rep_type.baseIsFloat())
      return (false);

    return (true);
  }

  /**
   * Returns a string in the specified format that describes the invariant.
   *
   * The generic format string is obtained from the subclass specific
   * get_format_str().  Instances of %var1% are replaced by the variable
   * name in the specified format.
   */
  public String format_using(OutputFormat format) {

    String fmt_str = get_format_str (format);

    VarInfo var1 = ppt.var_infos[0];
    String v1 = null;

    if (v1 == null)
      v1 = var1.name_using(format);

    fmt_str = UtilMDE.replaceString(fmt_str, "%var1%", v1);
    return (fmt_str);
  }

  public InvariantStatus check_modified (double x, int count) {
    if (eq_check (x))
      return (InvariantStatus.NO_CHANGE);
    else
      return (InvariantStatus.FALSIFIED);
  }

  public InvariantStatus add_modified (double x, int count) {
    return check_modified (x, count);
  }

  protected double computeConfidence() {
    return CONFIDENCE_JUSTIFIED;
  }

  public boolean isSameFormula (Invariant other) {
    assert other.getClass() == getClass();
    return (true);
  }
  public boolean isExclusiveFormula(Invariant other) {
    return false;
  }

  /**
   * All range invariants except Even and PowerOfTwo are obvious since they
   * represented by some version of OneOf or Bound.
   */
  public /*@Nullable*/ DiscardInfo isObviousDynamically (VarInfo[] vis) {

    return new DiscardInfo (this, DiscardCode.obvious,
                            "Implied by Oneof or Bound");
  }

  /**
   * Looks for a OneOf invariant over vis.  Used by Even and PowerOfTwo
   * to dynamically suppress those invariants if a OneOf exists
   */
  protected /*@Nullable*/ OneOfFloat find_oneof (VarInfo[] vis) {
    return (OneOfFloat) ppt.parent.find_inv_by_class (vis, OneOfFloat.class);
  }

  /**
   * Return a format string for the specified output format.  Each instance
   * of %varN% will be replaced by the correct name for varN.
   */
  public abstract String get_format_str (OutputFormat format);

  /**
   * Returns true if x and y don't invalidate the invariant.
   */
  public abstract boolean eq_check (double x);

  /**
   * Returns a list of prototypes of all of the range
   * invariants
   */
  public static List</*@Prototype*/ Invariant> get_proto_all () {

    List</*@Prototype*/ Invariant> result = new ArrayList</*@Prototype*/ Invariant>();
    result.add (EqualZero.get_proto());
    result.add (EqualOne.get_proto());
    result.add (EqualMinusOne.get_proto());
    result.add (GreaterEqualZero.get_proto());
    result.add (GreaterEqual64.get_proto());

    return (result);
  }

  /**
   * Internal invariant representing double scalars that are equal
   * to zero.  Used for non-instantiating suppressions.  Will never
   * print since OneOf accomplishes the same thing.
   */
  public static class EqualZero extends RangeFloat {

    // We are Serializable, so we specify a version to allow changes to
    // method signatures without breaking serialization.  If you add or
    // remove fields, you should change this number to the current date.
    static final long serialVersionUID = 20040113L;

    protected EqualZero (PptSlice ppt) {
      super (ppt);
    }

    protected /*@Prototype*/ EqualZero () {
      super ();
    }

    private static /*@Prototype*/ EqualZero proto;

    /** returns the prototype invariant **/
    public static /*@Prototype*/ EqualZero get_proto() {
      if (proto == null)
        proto = new /*@Prototype*/ EqualZero ();
      return proto;
    }

    /** Returns whether or not this invariant is enabled **/
    public boolean enabled() {
      return OneOfFloat.dkconfig_enabled;
    }

    /** instantiates the invariant on the specified slice **/
    public EqualZero instantiate_dyn (PptSlice slice) /*@Prototype*/ {
      return new EqualZero (slice);
    }

    public String get_format_str (OutputFormat format) {
      if (format == OutputFormat.SIMPLIFY)
        return ("(EQ 0 %var1%)");
      else
        return ("%var1% == 0");
    }

    public boolean eq_check (double x) {
      return (x == 0);
    }
  }

  /**
   * Internal invariant representing double scalars that are equal
   * to one.  Used for non-instantiating suppressions.  Will never
   * print since OneOf accomplishes the same thing
   */
  public static class EqualOne extends RangeFloat {

    // We are Serializable, so we specify a version to allow changes to
    // method signatures without breaking serialization.  If you add or
    // remove fields, you should change this number to the current date.
    static final long serialVersionUID = 20040113L;

    protected EqualOne (PptSlice ppt) {
      super (ppt);
    }

    protected /*@Prototype*/ EqualOne () {
      super ();
    }

    private static /*@Prototype*/ EqualOne proto;

    /** returns the prototype invariant **/
    public static /*@Prototype*/ EqualOne get_proto() {
      if (proto == null)
        proto = new /*@Prototype*/ EqualOne ();
      return proto;
    }

    /** Returns whether or not this invariant is enabled **/
    public boolean enabled() {
      return OneOfFloat.dkconfig_enabled;
    }

    /** instantiates the invariant on the specified slice **/
    public EqualOne instantiate_dyn (PptSlice slice) /*@Prototype*/ {
      return new EqualOne (slice);
    }

    public String get_format_str (OutputFormat format) {
      if (format == OutputFormat.SIMPLIFY)
        return ("(EQ 1 %var1%)");
      else
        return ("%var1% == 1");
    }

    public boolean eq_check (double x) {
      return (x == 1);
    }
  }

  /**
   * Internal invariant representing double scalars that are equal
   * to minus one.  Used for non-instantiating suppressions.  Will never
   * print since OneOf accomplishes the same thing
   */
  public static class EqualMinusOne extends RangeFloat {

    // We are Serializable, so we specify a version to allow changes to
    // method signatures without breaking serialization.  If you add or
    // remove fields, you should change this number to the current date.
    static final long serialVersionUID = 20040824L;

    protected EqualMinusOne (PptSlice ppt) {
      super (ppt);
    }

    protected /*@Prototype*/ EqualMinusOne () {
      super ();
    }

    private static /*@Prototype*/ EqualMinusOne proto;

    /** returns the prototype invariant **/
    public static /*@Prototype*/ EqualMinusOne get_proto() {
      if (proto == null)
        proto = new /*@Prototype*/ EqualMinusOne ();
      return proto;
    }

    /** Returns whether or not this invariant is enabled **/
    public boolean enabled() {
      return OneOfFloat.dkconfig_enabled;
    }

    /** instantiates the invariant on the specified slice **/
    public EqualMinusOne instantiate_dyn (PptSlice slice) /*@Prototype*/ {
      return new EqualMinusOne (slice);
    }

    public String get_format_str (OutputFormat format) {
      if (format == OutputFormat.SIMPLIFY)
        return ("(EQ -1 %var1%)");
      else
        return ("%var1% == -1");
    }

    public boolean eq_check (double x) {
      return (x == -1);
    }
  }

  /**
   * Internal invariant representing double scalars that are greater
   * than or equal to 0.  Used for non-instantiating suppressions.  Will never
   * print since Bound accomplishes the same thing
   */
  public static class GreaterEqualZero extends RangeFloat {

    // We are Serializable, so we specify a version to allow changes to
    // method signatures without breaking serialization.  If you add or
    // remove fields, you should change this number to the current date.
    static final long serialVersionUID = 20040113L;

    protected GreaterEqualZero (PptSlice ppt) {
      super (ppt);
    }

    protected /*@Prototype*/ GreaterEqualZero () {
      super ();
    }

    private static /*@Prototype*/ GreaterEqualZero proto;

    /** returns the prototype invariant **/
    public static /*@Prototype*/ GreaterEqualZero get_proto() {
      if (proto == null)
        proto = new /*@Prototype*/ GreaterEqualZero ();
      return proto;
    }

    /** Returns whether or not this invariant is enabled **/
    public boolean enabled() {
      return LowerBoundFloat.dkconfig_enabled;
    }

    /** instantiates the invariant on the specified slice **/
    public GreaterEqualZero instantiate_dyn (PptSlice slice) /*@Prototype*/ {
      return new GreaterEqualZero (slice);
    }

    public String get_format_str (OutputFormat format) {
      if (format == OutputFormat.SIMPLIFY)
        return ("(>= %var1% 0)");
      else
        return ("%var1% >= 0");
    }

    public boolean eq_check (double x) {
      return (x >= 0);
    }
  }

  /**
   * Internal invariant representing double scalars that are greater
   * than or equal to 64.  Used for non-instantiating suppressions.  Will never
   * print since Bound accomplishes the same thing
   */
  public static class GreaterEqual64 extends RangeFloat {

    // We are Serializable, so we specify a version to allow changes to
    // method signatures without breaking serialization.  If you add or
    // remove fields, you should change this number to the current date.
    static final long serialVersionUID = 20040113L;

    protected GreaterEqual64 (PptSlice ppt) {
      super (ppt);
    }

    protected /*@Prototype*/ GreaterEqual64 () {
      super ();
    }

    private static /*@Prototype*/ GreaterEqual64 proto;

    /** returns the prototype invariant **/
    public static /*@Prototype*/ GreaterEqual64 get_proto() {
      if (proto == null)
        proto = new /*@Prototype*/ GreaterEqual64 ();
      return proto;
    }

    /** Returns whether or not this invariant is enabled **/
    public boolean enabled() {
      return LowerBoundFloat.dkconfig_enabled;
    }

    /** instantiates the invariant on the specified slice **/
    public GreaterEqual64 instantiate_dyn (PptSlice slice) /*@Prototype*/ {
      return new GreaterEqual64 (slice);
    }

    public String get_format_str (OutputFormat format) {
      if (format == OutputFormat.SIMPLIFY)
        return ("(>= 64 %var1%)");
      else
        return ("%var1% >= 64");
    }

    public boolean eq_check (double x) {
      return (x >= 64);
    }
  }

}
